COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDCONST WISE1 WISE2 WISE3 ε PERSON
C00003 ENDMK
C⊗;
DECLARE INDCONST WISE1 WISE2 WISE3 ε PERSON;
DECLARE INDCONST RW ε WORLD;
DECLARE INDCONST WHITE1 WHITE2 WHITE3 εPROPOSITION;

AXIOM WISEMAN:
	T(WHITE1,RW)∧T(WHITE2,RW)∧T(WHITE3,RW),

	T(K(FOOL,KW(WISE1,WHITE2)),RW),
	T(K(FOOL,KW(WISE1,WHITE3)),RW),
	T(K(FOOL,KW(WISE2,WHITE1)),RW),
	T(K(FOOL,KW(WISE2,WHITE3)),RW),
	T(K(FOOL,KW(WISE3,WHITE1)),RW),
	T(K(FOOL,KW(WISE3,WHITE2)),RW),
	T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),RW),
	T(K(FOOL,KW(WISE3,KW(WISE2,WHITE2))),RW),
	T(K(FOOL,KW(WISE2,KW(WISE1,WHITE1))),RW),

	¬T(KW(WISE1,WHITE1),RW),
	¬T(KW(WISE2,WHITE2),RW);
;